|
| 1: |
|
le(0,y) |
→ true |
| 2: |
|
le(s(x),0) |
→ false |
| 3: |
|
le(s(x),s(y)) |
→ le(x,y) |
| 4: |
|
eq(0,0) |
→ true |
| 5: |
|
eq(0,s(y)) |
→ false |
| 6: |
|
eq(s(x),0) |
→ false |
| 7: |
|
eq(s(x),s(y)) |
→ eq(x,y) |
| 8: |
|
if(true,x,y) |
→ x |
| 9: |
|
if(false,x,y) |
→ y |
| 10: |
|
minsort(nil) |
→ nil |
| 11: |
|
minsort(cons(x,y)) |
→ cons(min(x,y),minsort(del(min(x,y),cons(x,y)))) |
| 12: |
|
min(x,nil) |
→ x |
| 13: |
|
min(x,cons(y,z)) |
→ if(le(x,y),min(x,z),min(y,z)) |
| 14: |
|
del(x,nil) |
→ nil |
| 15: |
|
del(x,cons(y,z)) |
→ if(eq(x,y),z,cons(y,del(x,z))) |
|
There are 12 dependency pairs:
|
| 16: |
|
LE(s(x),s(y)) |
→ LE(x,y) |
| 17: |
|
EQ(s(x),s(y)) |
→ EQ(x,y) |
| 18: |
|
MINSORT(cons(x,y)) |
→ MINSORT(del(min(x,y),cons(x,y))) |
| 19: |
|
MINSORT(cons(x,y)) |
→ DEL(min(x,y),cons(x,y)) |
| 20: |
|
MINSORT(cons(x,y)) |
→ MIN(x,y) |
| 21: |
|
MIN(x,cons(y,z)) |
→ IF(le(x,y),min(x,z),min(y,z)) |
| 22: |
|
MIN(x,cons(y,z)) |
→ LE(x,y) |
| 23: |
|
MIN(x,cons(y,z)) |
→ MIN(x,z) |
| 24: |
|
MIN(x,cons(y,z)) |
→ MIN(y,z) |
| 25: |
|
DEL(x,cons(y,z)) |
→ IF(eq(x,y),z,cons(y,del(x,z))) |
| 26: |
|
DEL(x,cons(y,z)) |
→ EQ(x,y) |
| 27: |
|
DEL(x,cons(y,z)) |
→ DEL(x,z) |
|
The approximated dependency graph contains 5 SCCs:
{17},
{16},
{27},
{23,24}
and {18}.